(set-option :opt.priority box)
(set-option :opt.optsmt_engine farkas)
(set-option :smt.phase_selection 6)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const i9 Int)
(declare-const i10 Int)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v22 Bool)
(declare-const v23 Bool)
(declare-const v24 Bool)
(declare-const v25 Bool)
(assert (or (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) v8 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4)))
(assert (or (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) v3 (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11)))
(assert (or v3 v2 v2))
(assert (or (xor (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) v20 v9 v16 v10) v8 (xor (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) v20 v9 v16 v10)))
(assert (or (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (and v16 (distinct 53 i8) v16 v3 v11 v7 v9 (and v0 (= i2 i10))) (xor (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) v20 v9 v16 v10)))
(assert (or (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) (or (>= (+ i2 7 38) i10) v9 (distinct 53 i8) v11 v9)))
(assert (or (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) v3 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4)))
(assert (or (or (>= (+ i2 7 38) i10) v9 (distinct 53 i8) v11 v9) (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) (xor (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) v20 v9 v16 v10)))
(assert (or (or (>= (+ i2 7 38) i10) v9 (distinct 53 i8) v11 v9) (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) v2))
(assert (or (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) v3 v8))
(assert (or (or (>= (+ i2 7 38) i10) v9 (distinct 53 i8) v11 v9) (and v16 (distinct 53 i8) v16 v3 v11 v7 v9 (and v0 (= i2 i10))) v2))
(assert (or (and v16 (distinct 53 i8) v16 v3 v11 v7 v9 (and v0 (= i2 i10))) v8 (or (>= (+ i2 7 38) i10) v9 (distinct 53 i8) v11 v9)))
(assert (or v2 (xor (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) v20 v9 v16 v10) (and v16 (distinct 53 i8) v16 v3 v11 v7 v9 (and v0 (= i2 i10)))))
(assert (or v8 (distinct (distinct 53 i8) v6 (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (distinct 53 i8) v20 v12 v7 v19 v6 v7 v11) (and v16 (distinct 53 i8) v16 v3 v11 v7 v9 (and v0 (= i2 i10)))))
(assert (or (and v16 (distinct 53 i8) v16 v3 v11 v7 v9 (and v0 (= i2 i10))) (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (and v16 (distinct 53 i8) v16 v3 v11 v7 v9 (and v0 (= i2 i10)))))
(assert (or (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4) (or (>= (+ i2 7 38) i10) v9 (distinct 53 i8) v11 v9) (xor v6 v12 v11 v18 v6 (distinct 53 i8) v7 v3 v7 v4)))
(assert (or v8 v2 (and v16 (distinct 53 i8) v16 v3 v11 v7 v9 (and v0 (= i2 i10)))))
(minimize (+ i2 i3))
(minimize (+ i2 i9))
(minimize (+ i3 i5))
(minimize (+ i3 i6))
(maximize (- i3 i7))
(minimize (+ i3 i9))
(minimize (+ i5 i9))
(minimize (+ i6 i7))
(minimize (+ i6 i9))
(maximize (- i7 i9))
(check-sat)
(exit)
